Reductions, intersection types, and explicit substitutions
Identifieur interne : 007894 ( Main/Exploration ); précédent : 007893; suivant : 007895Reductions, intersection types, and explicit substitutions
Auteurs : Dan Dougherty [États-Unis] ; Pierre Lescanne [France]Source :
- Mathematical Structures in Computer Science [ 0960-1295 ] ; 2003-02.
Abstract
This paper is part of a general programme of treating explicit substitutions as the primary λ-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction. We show that the terms that normalise by leftmost reduction and the terms that normalise by head reduction can each be characterised as the terms typable in a certain system. The relationship between typability and strong normalisation is subtly different from the classical case: we show that typable terms are strongly normalising but give a counterexample to the converse. Our notions of leftmost and head reduction are non-deterministic, and our normalisation theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalisation theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, our proofs do not rely on results from classical λ-calculus, which in our view is subordinate to the calculus of explicit substitution.
Url:
DOI: 10.1017/S0960129502003821
Affiliations:
- France, États-Unis
- Auvergne-Rhône-Alpes, Connecticut, Rhône-Alpes
- Lyon, Lyon 07
- École normale supérieure de Lyon
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000890
- to stream Istex, to step Curation: 000885
- to stream Istex, to step Checkpoint: 001883
- to stream Main, to step Merge: 007C72
- to stream Main, to step Curation: 007894
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Reductions, intersection types, and explicit substitutions</title>
<author><name sortKey="Dougherty, Dan" sort="Dougherty, Dan" uniqKey="Dougherty D" first="Dan" last="Dougherty">Dan Dougherty</name>
</author>
<author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Lyon</settlement>
<region type="region" nuts="2">Rhône-Alpes</region>
</placeName>
<orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:27071424204977ABACF636C52BD08B3C1590E09A</idno>
<date when="2003" year="2003">2003</date>
<idno type="doi">10.1017/S0960129502003821</idno>
<idno type="url">https://api.istex.fr/ark:/67375/6GQ-WNF4V7G4-V/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000890</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000890</idno>
<idno type="wicri:Area/Istex/Curation">000885</idno>
<idno type="wicri:Area/Istex/Checkpoint">001883</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001883</idno>
<idno type="wicri:doubleKey">0960-1295:2003:Dougherty D:reductions:intersection:types</idno>
<idno type="wicri:Area/Main/Merge">007C72</idno>
<idno type="wicri:Area/Main/Curation">007894</idno>
<idno type="wicri:Area/Main/Exploration">007894</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a">Reductions, intersection types, and explicit substitutions</title>
<author><name sortKey="Dougherty, Dan" sort="Dougherty, Dan" uniqKey="Dougherty D" first="Dan" last="Dougherty">Dan Dougherty</name>
<affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country>
<placeName><region type="state">Connecticut</region>
</placeName>
<wicri:cityArea>Department of Mathematics and Computer Science, Wesleyan University, Middletown</wicri:cityArea>
</affiliation>
</author>
<author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>Laboratoire de l'Informatique du Parallélisme, École Normale Supérieure de Lyon, 46, Allée d'Italie, 69364 Lyon 07</wicri:regionArea>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">Lyon 07</settlement>
</placeName>
<placeName><settlement type="city">Lyon</settlement>
<region type="region" nuts="2">Rhône-Alpes</region>
</placeName>
<orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Mathematical Structures in Computer Science</title>
<idno type="ISSN">0960-1295</idno>
<idno type="eISSN">1469-8072</idno>
<imprint><publisher>Cambridge University Press</publisher>
<pubPlace>Cambridge, UK</pubPlace>
<date type="published" when="2003-02">2003-02</date>
<biblScope unit="volume">13</biblScope>
<biblScope unit="issue">1</biblScope>
<biblScope unit="page" from="55">55</biblScope>
<biblScope unit="page" to="85">85</biblScope>
</imprint>
<idno type="ISSN">0960-1295</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0960-1295</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract">This paper is part of a general programme of treating explicit substitutions as the primary λ-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction. We show that the terms that normalise by leftmost reduction and the terms that normalise by head reduction can each be characterised as the terms typable in a certain system. The relationship between typability and strong normalisation is subtly different from the classical case: we show that typable terms are strongly normalising but give a counterexample to the converse. Our notions of leftmost and head reduction are non-deterministic, and our normalisation theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalisation theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, our proofs do not rely on results from classical λ-calculus, which in our view is subordinate to the calculus of explicit substitution.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>États-Unis</li>
</country>
<region><li>Auvergne-Rhône-Alpes</li>
<li>Connecticut</li>
<li>Rhône-Alpes</li>
</region>
<settlement><li>Lyon</li>
<li>Lyon 07</li>
</settlement>
<orgName><li>École normale supérieure de Lyon</li>
</orgName>
</list>
<tree><country name="États-Unis"><region name="Connecticut"><name sortKey="Dougherty, Dan" sort="Dougherty, Dan" uniqKey="Dougherty D" first="Dan" last="Dougherty">Dan Dougherty</name>
</region>
</country>
<country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name>
</region>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 007894 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 007894 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= ISTEX:27071424204977ABACF636C52BD08B3C1590E09A |texte= Reductions, intersection types, and explicit substitutions }}
This area was generated with Dilib version V0.6.33. |